feat(coq): L-S43 PowerStateSafety β Wave-11b power-gate FSM off-active overlap proof#800
Open
gHashTag wants to merge 1 commit into
Open
feat(coq): L-S43 PowerStateSafety β Wave-11b power-gate FSM off-active overlap proof#800gHashTag wants to merge 1 commit into
gHashTag wants to merge 1 commit into
Conversation
β¦e overlap proof Closes #799 Proves that the Wave-11b power-gate FSM never enters the illegal 'off-active overlap' state (pwr_en=0 AND clk_en=1 simultaneously), which would crash silicon. Deliverables: - docs/phd/theorems/igla/PowerStateSafety.v * Inductive pstate (OFF | WAKE | ACTIVE | SLEEP_REQ) * Definition pwr_en / clk_en / step / run * Theorem no_off_active_overlap: forall s, pwr_en s = false -> clk_en s = false * Lemma reachable_states_safe: all states in run init seq satisfy invariant * All proofs end Qed. β zero Admitted. - docs/phd/artifacts/coq_citation_map.json * PowerStateSafety.no_off_active_overlap -> power_gate_fsm.v * PowerStateSafety.reachable_states_safe -> power_gate_fsm.v Verification: coqc 8.20.1 exit 0 Anchor: phi^2 + phi^-2 = 3 License: Apache-2.0
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #799
Summary
Formal Coq proof that the Wave-11b power-gate FSM never enters the illegal "off-active overlap" state where
pwr_en=0 AND clk_en=1simultaneously β a condition that would crash silicon.Deliverables
docs/phd/theorems/igla/PowerStateSafety.vInductive pstate:OFF | WAKE | ACTIVE | SLEEP_REQDefinition pwr_en: power enable signal (false only in OFF)Definition clk_en: clock enable signal (true only in ACTIVE)Definition step: deterministic FSM transition functionFixpoint run: trace all visited states over an input sequenceTheorem
no_off_active_overlap:forall s : pstate, pwr_en s = false -> clk_en s = falseProved by
destruct s+reflexivity/discriminate.Lemma
reachable_states_safe:forall (init : pstate) (seq : list input) (s : pstate), In s (run init seq) -> pwr_en s = false -> clk_en s = falseProved by structural induction over the input sequence.
All proofs end
Qed.β zeroAdmitted.docs/phd/artifacts/coq_citation_map.jsonNew file mapping:
PowerStateSafety.no_off_active_overlapβpower_gate_fsm.vPowerStateSafety.reachable_states_safeβpower_gate_fsm.vVerification
Anchor
ΟΒ² + Οβ»Β² = 3
License
Apache-2.0
Author
Dmitrii Vasilev admin@t27.ai